Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	minus_active(0,y)	→ 0
2:	mark(0)	→ 0
3:	minus_active(s(x),s(y))	→ minus_active(x,y)
4:	mark(s(x))	→ s(mark(x))
5:	ge_active(x,0)	→ true
6:	mark(minus(x,y))	→ minus_active(x,y)
7:	ge_active(0,s(y))	→ false
8:	mark(ge(x,y))	→ ge_active(x,y)
9:	ge_active(s(x),s(y))	→ ge_active(x,y)
10:	mark(div(x,y))	→ div_active(mark(x),y)
11:	div_active(0,s(y))	→ 0
12:	mark(if(x,y,z))	→ if_active(mark(x),y,z)
13:	div_active(s(x),s(y))	→ if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)
14:	if_active(true,x,y)	→ mark(x)
15:	minus_active(x,y)	→ minus(x,y)
16:	if_active(false,x,y)	→ mark(y)
17:	ge_active(x,y)	→ ge(x,y)
18:	if_active(x,y,z)	→ if(x,y,z)
19:	div_active(x,y)	→ div(x,y)

There are 13 dependency pairs:


20:	MINUS_ACTIVE(s(x),s(y))	→ MINUS_ACTIVE(x,y)
21:	MARK(s(x))	→ MARK(x)
22:	MARK(minus(x,y))	→ MINUS_ACTIVE(x,y)
23:	MARK(ge(x,y))	→ GE_ACTIVE(x,y)
24:	GE_ACTIVE(s(x),s(y))	→ GE_ACTIVE(x,y)
25:	MARK(div(x,y))	→ DIV_ACTIVE(mark(x),y)
26:	MARK(div(x,y))	→ MARK(x)
27:	MARK(if(x,y,z))	→ IF_ACTIVE(mark(x),y,z)
28:	MARK(if(x,y,z))	→ MARK(x)
29:	DIV_ACTIVE(s(x),s(y))	→ IF_ACTIVE(ge_active(x,y),s(div(minus(x,y),s(y))),0)
30:	DIV_ACTIVE(s(x),s(y))	→ GE_ACTIVE(x,y)
31:	IF_ACTIVE(true,x,y)	→ MARK(x)
32:	IF_ACTIVE(false,x,y)	→ MARK(y)

The approximated dependency graph contains 3 SCCs: {24}, {20} and {21,25-29,31,32}.

Consider the SCC {24}. There are no usable rules. By taking the AF π with π(GE_ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 24 is strictly decreasing.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(MINUS_ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {21,25-29,31,32}. By taking the AF π with π(mark) = π(MARK) = π(minus) = π(minus_active) = 1, π(ge) = π(ge_active) = [ ], π(div) = π(div_active) = π(DIV_ACTIVE) = [1] and π(IF_ACTIVE) = [2, 3] together with the lexicographic path order with precedence div_active ≻ if_active ≻ IF_ACTIVE, div_active ≻ s ≻ 0, s ≻ ge_active ≻ false, ge_active ≻ true, ge_active ≈ ge, if_active ≈ if and div_active ≈ div ≈ DIV_ACTIVE, the rules in {1,2,4,6,8-10,12,15,17-19,25} are weakly decreasing and the rules in {3,5,7,11,13,14,16,21,26-29,31,32} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (20.27 seconds) --- May 4, 2006